package assignment2;

public class GameBoard {
  
    // GHOST VARIABLES
  
    /**
     * These ghost variables are used to define a state machine, this state machine is used to model the life-cycle of the board.
     * 
     * The various constraints below define what transitions are possible under which circumstances.
     */
  
    /**
     * The ghost variable <code>status</code> is used to represent the current state of the board.
     */
  
    //@ static ghost int status = UNINITIALIZED;
  
    /**
     * Initially the board is in the state <code>UNINITIALIZED</code>.
     */
  
    //@ static final ghost int UNINITIALIZED = 0;
  
    /**
     * The board is in state <code>NOT_STARTED</code> when it has just been initialized or when the board has been reset using 
     * <code>clearboard()</code>. No move has been made yet.
     */
  
    //@ static final ghost int NOT_STARTED = 1;
  
    /**
     * The board is in state <code>READY_FOR_MOVE</code> when the next player must make a move.
     */
  
    //@ static final ghost int READY_FOR_MOVE = 2;
  
    /**
     * The board is in state <code>BUSY_UPDATING</code> when <code>gravity</code> has been enabled and the board must be updated 
     * to model the pieces 'dropping down'.
     */
  
    //@ static final ghost int BUSY_UPDATING = 3;
  
    /**
     * The board is in state <code>CHECKING_FOR_WINNER</code> when a move has been made or the board has finished updating and the 
     * board must be checked for a winner.
     */
  
    //@ static final ghost int CHECKING_FOR_WINNER = 4;
  
    /**
     * The board is in state <code>FINISHED</code> when the game is over because either there is a winner or the board is full.
     */
  
    //@ static final ghost int FINISHED = 5;
  
    // MODEL VARIABLES ------------------------------------------------------------------------------------------------
  
    /**
     * This model variable is true when all squares of the board are <code>Empty</code>.
     */
  
    //@ model boolean board_empty;
    //@ represents board_empty <- (\forall int i, j; 0 <= i && i < width && 0 <= j && j < height; board[i][j] == Empty);
    
    /**
     * This model variable is true when all squares of the board are either <code>Cross</code> or <code>Circle</code>.
     */
  
    //@ model boolean board_full;
    //@ represents board_full <- (\forall int i, j; 0 <= i && i < width && 0 <= j && j < height; board[i][j] == Cross || board[i][j] == Circle);
    
    /**
     * This model variable is true when a winner can be found for a particular column of the board.
     */
  
    //@ model boolean board_of_won_game;
    //@ represents board_of_won_game <- (\exists int i; 0 <= i && i < width; winnerOfColumn(i) != Empty);
  
    /**
     * This model variable is true when there is no winner nor is the board full.
     */
  
    //@ model boolean board_of_game_in_progress;
    //@ represents board_of_game_in_progress <- !board_of_won_game && !board_full;
  
    /**
     * This model variable is true when the game is in its initial state.
     */
  
    //@ model boolean game_reset_and_board_empty;
    //@ represents game_reset_and_board_empty <- board_empty && gravity == false && turn == Cross && count == 0 && winner == Empty && busy == false;
  
    /**
     * This model variable is true when the board has valid dimensions, i.e., when the width and the height of the board is correct.
     */
  
    //@ model boolean board_has_valid_dimensions;
    //@ represents board_has_valid_dimensions <- board.length == width && (\forall int i; 0 <= i && i < width; board[i] != null && board[i].length == height);
  
    // INVARIANTS -----------------------------------------------------------------------------------------------------
    
    /**
     * This invariant ensures that the board is always in a valid state, i.e., in one of the states defined above.
     */
  
    //@ invariant status == UNINITIALIZED || status == NOT_STARTED || status == READY_FOR_MOVE || status == BUSY_UPDATING || status == CHECKING_FOR_WINNER || status == FINISHED;
  
    /**
     * This invariant ensures that the width of the board is always greater than zero.
     */
  
    //@ invariant width > 0;
  
    /**
     * This invariant ensures that the height of the board is always greater than zero.
     */
    
    //@ invariant height > 0;
  
    /**
     * This invariant ensures that the width of the board is equal to <code>width</code>.
     */
  
    //@ invariant board.length == width;
  
    /**
     * This invariant ensures that all columns of the board are present and contain exactly <code>height</code> squares.
     */
  
    //@ invariant (\forall int i; 0 <= i && i < width; board[i] != null && board[i].length == height);
  
    /**
     * This invariant ensures that all squares of the board are either <code>Empty</code>, <code>Circle</code> or <code>Cross</code>.
     */
  
    //@ invariant (\forall int i, j; 0 <= i && i < width && 0 <= j && j < height; board[i][j] == Empty || board[i][j] == Circle || board[i][j] == Cross);
  
    /**
     * This invariant ensures that <code>turn</code> is either <code>Cross</code> or <code>Circle</code>.
     */
  
    //@ invariant turn == Cross || turn == Circle;
  
    /**
     * This invariant ensures that <code>count</code>, which models the number of occupied squares, is between (and including) 0 
     * and the total number of squares, which is equal to <code>width * height</code>.
     */
    
    //@ invariant count >= 0 && count <= width * height;
  
    /**
     * This invariant ensures that there is either is no winner (modeled by setting <code>winner</code> to <code>Empty</code>), or 
     * the winner is <code>Cross</code> or <code>Circle</code>.
     */
    
    //@ invariant winner == Cross || winner == Circle || winner == Empty;
  
    /**
     * This invariant ensures that <code>goal</code>, which denotes the number of squares in a row that the winner must have, is 
     * greater than zero.
     */
    
    //@ invariant goal > 0;
  
    // INITIALLY CLAUSES ----------------------------------------------------------------------------------------------
  
    /**
     * This initially clause ensures that after the constructor has been executed, the board is in the initial state (as modelled 
     * by the <code>game_reset_and_board_empty</code> model variable). 
     */
  
    //@ initially game_reset_and_board_empty;
  
    // CONSTRAINTS ----------------------------------------------------------------------------------------------------

    /**
     * This constraint ensures that from the state <code>UNINITIALIZED<code> the board can either move to the state <code>NOT_STARTED<code> 
     * (by executing the constructor) or remain in the state <code>UNINITIALIZED<code>. 
     */
  
    //@ constraint \old(status == UNINITIALIZED) ==> (status == UNINITIALIZED || status == NOT_STARTED);
  
    /**
     * This constraint ensures that from the state <code>NOT_STARTED<code> the board can either move to the states <code>BUSY_UPDATING<code> 
     * (by performing a move when <code>gravity</code> is enabled), <code>CHECKING_FOR_WINNER<code> (by performing a move when <code>gravity</code>
     * is not enabled) and <code>FINISHED</code> (actually, this can never happen as at least one move is required, but this makes the
     * specification of the methods <code>gameOver</code> and <code>status</code> (which uses <code>gameOver</code> easier), or remain 
     * in the state <code>NOT_STARTED<code>. 
     */
  
    //@ constraint \old(status == NOT_STARTED) ==> (status == NOT_STARTED || status == BUSY_UPDATING || status == CHECKING_FOR_WINNER || status == FINISHED);
  
    /**
     * This constraint ensures that from the state <code>READY_FOR_MOVE</code> the board can either move to the states <code>BUSY_UPDATING<code>
     * (by performing a move when <code>gravity</code> is enabled), <code>CHECKING_FOR_WINNER<code> (by performing a move when <code>gravity</code>
     * is not enabled) or <code>FINISHED</code> (actually, this can never happen as the board will only move from state <code>CHECKING_FOR_WINNER</code>
     * to <code>FINISHED</code>, but this makes the specification of the methods <code>gameOver</code> and <code>status</code> (which 
     * uses <code>gameOver</code>) easier), or remain in the state <code>READY_FOR_MOVE<code>. Furthermore, the board can move to the state
     * <code>NOT_STARTED</code> when <code>clearboard</code> is called.
     */
  
    //@ constraint \old(status == READY_FOR_MOVE) ==> (status == READY_FOR_MOVE || status == BUSY_UPDATING || status == CHECKING_FOR_WINNER || status == NOT_STARTED || status == FINISHED);
  
    /**
     * This constraint ensures that from the state <code>BUSY_UPDATING</code> the board can either move to the states <code>CHECKING_FOR_WINNER</code>
     * (when it has finished updating, i.e., when <code>notDone</code> returns false) or <code>NOT_STARTED</code> (after a call to <code>clearboard</code>,
     * or remain in the state <code>BUSY_UPDATING<code>.
     */
  
    //@ constraint \old(status == BUSY_UPDATING) ==> (status == BUSY_UPDATING || status == CHECKING_FOR_WINNER || status == NOT_STARTED);
  
    /**
     * This constraint ensures that from the state <code>CHECKING_FOR_WINNER</code> the board can either move to the state <code>READY_FOR_MOVE</code>
     * (when no winner has been found and the board is not yet fully filled) or the state <code>FINISHED</code> (when a winner has been found or
     * the board is fully filled). Furthermore, the board can move to the state <code>NOT_STARTED</code> after a call to <code>clearboard</code>.
     */
  
    //@ constraint \old(status == CHECKING_FOR_WINNER) ==> (status == CHECKING_FOR_WINNER || status == READY_FOR_MOVE || status == FINISHED || status == NOT_STARTED)
    
    /**
     * This constraint ensures that from the state <code>FINISHED</code> the board can move to the state <code>NOT_STARTED</code> (after a call
     * to <code>clearboard</code>) or remain in the state <code>FINISHED</code>.
     */
  
    //@ constraint \old(status == FINISHED) ==> (status == FINISHED || status == NOT_STARTED);
  
    /**
     * This constraint ensures that the board can only start updating itself (i.e., make the pieces 'drop down') when <code>gravity</code> has
     * been enabled.
     */
  
    //@ constraint (\old(status == NOT_STARTED || status == READY_FOR_MOVE) && (status == BUSY_UPDATING)) ==> gravity;
  
    /**
     * This constraint ensures that the board can only start checking for a winner directly after a move, without updating itself,
     * when <code>gravity</code> has not been enabled.
     */
  
    //@ constraint (\old(status == NOT_STARTED || status == READY_FOR_MOVE) && (status == CHECKING_FOR_WINNER)) ==> !gravity;
  
    /**
     * This constraint ensures that the board can only stop updating when all pieces have 'dropped down' completely, as indiciated by
     * the <code>notDone</code> method.
     */
  
    //@ constraint ((\old(status == BUSY_UPDATING)) && (status == CHECKING_FOR_WINNER)) ==> !notDone();
  
    /**
     * This constraint ensures that <code>gravity</code> can only be enabled (or disabled) when the board is in the state <code>NOT_STARTED</code>,
     * i.e., when no move has been made yet.
     */
  
    //@ constraint (\old(gravity) != gravity) ==> (status == NOT_STARTED);
  
    // CLASS VARIABLES ------------------------------------------------------------------------------------------------

    public static final byte Empty=0;
    public static final byte Cross=1;
    public static final byte Circle=2;
    
    // INSTANCE VARIABLES ---------------------------------------------------------------------------------------------
    
    private /*@ non_null @*/ byte[][] board;
    
    private /*@ spec_public @*/ int width,height;
    
    private /*@ spec_public @*/ byte turn;
    
    private /*@ spec_public @*/ int count;
    
    private byte winner=Empty;
    
    private /*@ spec_public @*/ int goal;
    
    private /*@ spec_public @*/ boolean gravity;
    
    private /*@ spec_public @*/ boolean busy;
    
    // METHODS --------------------------------------------------------------------------------------------------------
    
    /**
     * Moves the board from state <code>UNINITIALIZED</code> to state <code>NOT_STARTED</code>.
     */
    
    /*@ normal_behavior
      @   requires    status == UNINITIALIZED &&
      @               width > 0 &&
      @               height > 0 &&
      @               goal > 0;
      @   ensures     status == NOT_STARTED &&
      @               this.width == width &&
      @               this.height == height && 
      @               this.goal == goal;
      @*/
    public GameBoard(int width,int height,int goal){
      this.width=width;
      this.height=height;
      this.goal=goal;
      this.gravity=false;
      board=new byte[width][height];
      turn=Cross;
      busy = false;
      //@ assume 0 < width * height;
      clearboard();
    }

   /**
    * This method has been rewritten because ESC/Java struggles with loop invariants that specify properties of two-dimensional arrays.
    * 
    * Note that you cannot clear a board while it's in the middle of being updated. When a board is cleared, the game is reset to its initial state.
    */
    
    /*@ normal_behavior
      @   requires    status != BUSY_UPDATING;
      @   ensures     status == NOT_STARTED &&
      @               game_reset_and_board_empty;
      @*/
    public void clearboard() {      
        //@ loop_invariant 0 <= i && i <= width;
        //@ loop_invariant (\forall int k, l; 0 <= k && k < i && 0 <= l && l < height; board[k][l] == Empty);
        for (int i = 0; i < width; i++){
          clearcolumn(i);
        }
        
        count = 0;
        winner = Empty;
        turn = Cross;
        busy = false;
        gravity = false;
        //@ set status = NOT_STARTED;
    }
    
    /**
     * Auxiliary method for <code>clearboard</code>. This method was required because ESC/Java struggles with loop invariants that specify
     * properties of two-dimensional arrays.
     */
    
    /*@ normal_behavior
      @   requires    status != BUSY_UPDATING &&
      @               0 <= x && x < width;
      @   ensures     status == \old(status) &&
      @               (\forall int i; 0 <= i && i < height; board[x][i] == Empty);
      @*/
    private void clearcolumn(int x) {
      //@ loop_invariant 0 <= i && i <= height;
      //@ loop_invariant (\forall int j; 0 <= j && j < i; board[x][j] == Empty);
      for (int i = 0; i < height; i++) {
        clear(x, i);
      }
    }
    
    /**
     * Auxiliary method for <code>clearboard</code>. This method was required because ESC/Java struggles with loop invariants that specify
     * properties of two-dimensional arrays.
     */
    
    /*@ normal_behavior
      @   requires    status != BUSY_UPDATING &&
      @               0 <= x && x < width &&
      @               0 <= y && y < height;
      @   ensures     status == \old(status) &&
      @               board[x][y] == Empty;
      @*/
    private void clear(int x, int y) {
        board[x][y] = Empty;
    }
    
    /**
     * Self-explanatory.
     */
    
    /*@ normal_behavior
      @   requires    status == NOT_STARTED;
      @   ensures     status == \old(status) &&
      @               this.gravity == gravity;
      @*/
    public void setGravity(boolean gravity) {
      this.gravity = gravity;
    }
    
    /**
     * We only allow moves to be performed when the board is in state <code>NOT_STARTED</code> or <code>READY_FOR_MOVE</code>. We also
     * require that the board is not fully filled yet by requiring that <code>count < width * height</code> and that the model
     * variable <code>board_of_game_in_progress</code> is true. When the move has been performed, the board moves either to state
     * <code>BUSY_UPDATING</code> (when <code>busy</code>, and thus <code>gravity</code> is true, and therefore the 'pieces' have to drop)
     * or the state <code>CHECKING_FOR_WINNER</code>. Note that after a move has been performed, the board can be either filled completely
     * (as modelled by <code>board_full</code>) or have a winner (as modelled by <code>board_of_won_game</code>) or neither (as modelled by 
     * <code>board_of_game_in_progress</code>).
     */
    
    /*@ normal_behavior
      @   requires    (status == NOT_STARTED || status == READY_FOR_MOVE) && 
      @               0 <= x && x < width &&
      @               0 <= y && y < height &&
      @               board[x][y] == Empty &&
      @               count < width * height &&
      @               board_of_game_in_progress;
      @   ensures     (busy ? status == BUSY_UPDATING : status == CHECKING_FOR_WINNER) &&
      @               busy == gravity &&
      @               board[x][y] == \old(turn) &&
      @               count == \old(count) + 1 &&
      @               \old(turn) == Cross ? turn == Circle : turn == Cross &&
      @               (board_of_game_in_progress || board_full || board_of_won_game);
      @*/
    public void move(int x,int y){
        count++;
        board[x][y]=turn;
        busy=gravity;
        //@ set status = busy ? BUSY_UPDATING : CHECKING_FOR_WINNER;
        switch(turn){
            case Cross:
                turn=Circle;
                break;
            case Circle:
                turn=Cross;
                break;
        }
    }
    
    /**
     * Self-explanatory.
     */
    
    /*@ normal_behavior
      @   requires    status != UNINITIALIZED;
      @   ensures     status == \old(status) &&
      @               \result == busy;
      @*/
    public /*@ pure @*/ boolean dropping() {
        return busy;
    }
    
    /**
     * The condition of the while-loop has been rewritten to use <code>i + l * di</code> rather than <code>(i + l) * di</code>. This was a bug.
     * 
     * The requirements are trivial. As for the postconditions, we ensure (among other things) the following:
     * 
     * 1. The result will be greater than zero and smaller than <code>goal</code>.
     * 2. The result is such that it describes a valid sequence of squares, i.e., it does not cross any boundaries of the board.
     * 3. The described sequence of squares all have the same symbol (<code>Cross</code> or <code>Circle</code>), e.g., if
     *    the result is four, then there are four squares in a row that have the same symbol, starting from square (i, j).
     * 4. The described sequence of squares is maximal (with respect to <code>goal</code>. That is, if the result is four, then
     *    there is no row of five squares or more that have the same symbol, starting from square (i, j), unless goal is also four.
     */
    
    /*@ normal_behavior
      @   requires    status != UNINITIALIZED &&
      @               0 <= i && i < width &&
      @               0 <= j && j < height &&
      @               0 <= di && di <= 1 &&
      @               -1 <= dj && dj <= 1;
      @   ensures     status == \old(status) &&
      @               (\result > 0 && \result <= goal) &&
      @               (0 <= i + ((\result - 1) * di) && i + ((\result - 1) * di) < width) &&
      @               (0 <= j + ((\result - 1) * dj) && j + ((\result - 1) * dj) < height) &&
      @               (\forall int k; 0 <= k && k < \result; board[i][j] == board[i + (k * di)][j + (k * dj)]) &&
      @               (\result < goal ==> (
      @                 !(0 <= i + (\result * di) && i + (\result * di) < width) ||
      @                 !(0 <= j + (\result * dj) && j + (\result * dj) < height) ||
      @                 board[i][j] != board[i + (\result * di)][j + (\result * dj)]
      @               ));
      @*/
    private /*@ pure @*/ int check_row(int i,int j,int di,int dj){
      int l = 1;
      
      //@ loop_invariant 1 <= l && l <= goal;
      //@ loop_invariant 0 <= i + ((l - 1) * di) && i + ((l - 1) * di) < width;
      //@ loop_invariant 0 <= j + ((l - 1) * dj) && j + ((l - 1) * dj) < height;
      //@ loop_invariant (\forall int k; 0 <= k && k < l; board[i][j] == board[i + (k * di)][j + (k * dj)]);
      while ( l<goal &&
              0 <= i+l*di && i+l*di < width &&
              0 <= j+l*dj && j+l*dj < height &&
              board[i][j]==board[i+l*di][j+l*dj]
            ) {
        l++;
      }
      
      return l;
    }
    
    /**
     * The requirements are trivial. We ensure that the result is either <code>Empty</code>, <code>Cross</code> or <code>Circle</code>. Furthermore,
     * when the result is <code>Empty</code>, we ensure that there is no winner for the given column (as identified by <code>i</code>), when it is
     * <code>Cross</code>, there is a sequence of (at least) <code>goal</code> goal squares that have symbol <code>Cross</code>, starting from
     * a square in the <code>i'th</code> column, and thus <code>Cross</code> is a winner for that column. The case for <code>Circle</code> is of course
     * symmetrical.
     */

    /*@ normal_behavior
      @   requires    status != UNINITIALIZED && 
      @               0 <= x && x < width;
      @   ensures     status == \old(status) &&   
      @               (\result == Empty || \result == Cross || \result == Circle) &&
      @               ((\result == Empty) ==> (\forall int i; 0 <= i && i < height; board[x][i] == Empty || !(check_row(x,i,0,1) == goal || check_row(x,i,1,1) == goal || check_row(x,i,1,0) == goal || check_row(x,i,1,-1) == goal))) &&
      @               ((\result == Cross) ==> (\exists int i; 0 <= i && i < height; board[x][i] == Cross && (check_row(x,i,0,1) == goal || check_row(x,i,1,1) == goal || check_row(x,i,1,0) == goal || check_row(x,i,1,-1) == goal))) &&
      @               ((\result == Circle) ==> (\exists int i; 0 <= i && i < height; board[x][i] == Circle && (check_row(x,i,0,1) == goal || check_row(x,i,1,1) == goal || check_row(x,i,1,0) == goal || check_row(x,i,1,-1) == goal)));
      @*/
  	private /*@ pure @*/ byte winnerOfColumn(int x) {
  		byte winner_ = Empty;
  		int y = 0;
  		
  		//@ loop_invariant 0 <= y && y <= height;
  		//@ loop_invariant winner_ == Empty || winner_ == Cross || winner_ == Circle;
  		//@ loop_invariant (winner_ == Empty) ==> (\forall int i; 0 <= i && i < y; board[x][i] == Empty || !(check_row(x,i,0,1) == goal || check_row(x,i,1,1) == goal || check_row(x,i,1,0) == goal || check_row(x,i,1,-1) == goal));
  		//@ loop_invariant (winner_ == Cross) ==> (\exists int i; 0 <= i && i < height; board[x][i] == Cross && (check_row(x,i,0,1) == goal || check_row(x,i,1,1) == goal || check_row(x,i,1,0) == goal || check_row(x,i,1,-1) == goal));
      //@ loop_invariant (winner_ == Circle) ==> (\exists int i; 0 <= i && i < height; board[x][i] == Circle && (check_row(x,i,0,1) == goal || check_row(x,i,1,1) == goal || check_row(x,i,1,0) == goal || check_row(x,i,1,-1) == goal));
  		for(y=0;y<height;y++){
  			if (board[x][y] !=Empty &&
  				(check_row(x,y,0,1) == goal || check_row(x,y,1,1) == goal ||
  				 check_row(x,y,1,0) == goal || check_row(x,y,1,-1) == goal))
  			{
  				winner_ = board[x][y];
  			}
  		}
  		return winner_;
  	}

    
    /**
     * This method has been rewritten to check for possible winners when the board is full. This wasn't the case before, and therefore was a bug.
     * 
     * Once again, the requirements are trivial. As for the postconditions, we ensure the following:
     * 
     * 1. When the result is true, i.e., when a winner has been found or the board is full, the new state of the board is <code>FINISHED</code>.
     * 2. When the result is false, i.e., when no winner has been found and the board is not full, the new state of the board <code>READY_FOR_MOVE</code>
     *    in case the method was called from state <code>CHECKING_FOR_WINNER</code>, and equal to the old state otherwise.
     * 3. When winner equals <code>Empty</code>, there is no winner.
     * 4. When winner equals <code>Cross</code>, the winner is <code>Cross</code> as there is a column from which a row of <code>goal</code>
     *    squares with <code>Cross</code> starts.
     * 5. When winner equals <code>Circle</code>, the winner is <code>Circle</code> as there is a column from which a row of <code>goal</code>
     *    squares with <code>Circle</code> starts.
     */
    
  	/*@ normal_behavior
  	  @   requires    status != UNINITIALIZED &&
  	  @               status != BUSY_UPDATING;
  	  @   ensures     (\result ==> (status == FINISHED)) &&
  	  @               ((!\result && (\old(status) == CHECKING_FOR_WINNER)) ==> (status == READY_FOR_MOVE)) &&
  	  @               ((!\result && (\old(status) != CHECKING_FOR_WINNER)) ==> (status == \old(status))) &&       
  	  @               ((winner == Empty) ==> ((\result == (count == width * height)) && (\forall int i; 0 <= i && i < width; winnerOfColumn(i) == Empty))) &&
  	  @               ((winner == Cross) ==> (\result && (\exists int i; 0 <= i && i < width; winnerOfColumn(i) == Cross))) &&
  	  @               ((winner == Circle) ==>(\result && (\exists int i; 0 <= i && i < width; winnerOfColumn(i) == Circle)));
  	  @*/
    public boolean gameOver() {
      byte winner_ = Empty;
      int x=0;
      
      //@ loop_invariant 0 <= x && x <= width;
      //@ loop_invariant winner_ == Empty || winner_ == Cross || winner_ == Circle;
      //@ loop_invariant (winner_ == Empty) ==> (\forall int i; 0 <= i && i < x; winnerOfColumn(i) == Empty);
      //@ loop_invariant (winner_ == Cross) ==> (\exists int i; 0 <= i && i < x; winnerOfColumn(i) == Cross);
      //@ loop_invariant (winner_ == Circle) ==> (\exists int i; 0 <= i && i < x; winnerOfColumn(i) == Circle);
      for(x=0;x<width;x++){
          byte w = winnerOfColumn(x);
          if(w != Empty) {
            winner_ = w;
          }
      }
      
      /**
       * See below.
       */
      
      //@ assert (winner_ == Empty) ==> (\forall int i; 0 <= i && i < width; winnerOfColumn(i) == Empty);
      //@ assert (winner_ == Cross) ==> (\exists int i; 0 <= i && i < width; winnerOfColumn(i) == Cross);
      //@ assert (winner_ == Circle) ==> (\exists int i; 0 <= i && i < width; winnerOfColumn(i) == Circle);
      
      winner = winner_;
      
      boolean result = winner != Empty || count==width*height;
      
      //@ set status = (result ? FINISHED : ((status == CHECKING_FOR_WINNER) ? READY_FOR_MOVE : status));
      
      /**
       * We have to add these assumes here because ESC/Java incorrectly assumes that the assignment to the instance variable
       * <code>winner</code> above can somehow influence the result of a <code>winnerOfColumn</code> call. Note that all loop 
       * variables of the above loop do hold after the loop and before the assignment to <code>winner</code>, as can be verified
       * by checking the above asserts.
       */
      
      //@ assume (winner == Empty) ==> (\forall int i; 0 <= i && i < width; winnerOfColumn(i) == Empty);
      //@ assume (winner == Cross) ==> (\exists int i; 0 <= i && i < width; winnerOfColumn(i) == Cross);
      //@ assume (winner == Circle) ==> (\exists int i; 0 <= i && i < width; winnerOfColumn(i) == Circle);
      
      return result;
    }

    /**
     * field() requires the status not to be UNINITIALIZED.
     * The requirements on x and y prevent ArrayIndexOutOfBoundsExceptions.
     * field() ensures GameBoard remains in the same status.
     * The result is equal to board[x][y].
     */
    /*@ normal_behavior
      @   requires    status != UNINITIALIZED &&
      @               0 <= x && x < width &&
      @               0 <= y && y < height;
      @   ensures     status == \old(status) &&
      @               \result == board[x][y];
      @*/
    public /*@ pure */ byte field(int x,int y){
        return board[x][y];
    }
    
    /**
     * empty_below() requires the status not to be UNINITIALIZED.
     * Requirements on x and y prevent ArrayOutOfBoundsExceptions.
     * This method is pure, because it is used in the specification of notDone().
     * empty_below() ensures the status of GameBoard remains the same. 
     * The result depends on whether a tile which is not Empty has a tile below it which is Empty.
     */
    /*@ normal_behavior
      @   requires    status != UNINITIALIZED &&
      @               0 <= x && x < width &&
      @               0 <= y && y < height - 1;
      @   ensures     status == \old(status) &&
      @               (\result == (board[x][y] != Empty && board[x][y + 1] == Empty));
      @*/
    private /*@ pure @*/ boolean empty_below(int x, int y) {
    	return board[x][y]!= Empty && board[x][y+1]==Empty;
    }
    
    /**
     * notDone() requires the status not to be UNINITIALIZED.
     * notDone() ensures the status remains the same. 
     * Furthermore the result depends on whether a tile is empty below another tile which is not Empty.
     */
    /*@ normal_behavior
      @   requires    status != UNINITIALIZED;
      @   ensures     (status == \old(status)) &&
      @               (\result == (\exists int i, j; 0 <= i && i < width && 0 <= j && j < height - 1; empty_below(i, j)));
      @*/
    public /*@ pure @*/ boolean notDone(){
      //@ loop_invariant 0 <= x && x <= width;
      //@ loop_invariant (\forall int i, j; 0 <= i && i < x && 0 <= j && j < height - 1; !empty_below(i, j)); 
      for(int x=0;x<width;x++){
        //@ loop_invariant -1 <= y && y < height - 1;
        //@ loop_invariant (\forall int i; i > y && i < height - 1; !empty_below(x, i)); 
        for(int y=height-2;y>=0;y--){
          if (empty_below(x,y)) {
            return true;
          }
        }
      }
      return false;
    }
    
    /**
     * This method has been rewritten because ESC/Java struggles with loop invariants that specify properties of two-dimensional arrays.
     * We introduces three new methods, namely assignColumn, zero and assign. Furthermore, the conditions in the while-loop have been re-ordered,
     * previuously the check on <code>bottom</code> was performed after <code>board[x][bottom]</code> was accessed, which could lead to
     * an <code>ArrayIndexOutOfBoundsException</code>, which obviously was a bug. 
     * update() requires the status to be BUSY_UPDATING, because this method can only be called when tokens fall down.
     * update() ensures the status to be BUSY_UPDATING or CHECKING_FOR_WINNER depending on <code>busy</code> (busy is set to notDone()).
     */
    
    /*@ normal_behavior
      @   requires    status == BUSY_UPDATING;
      @   ensures     (busy ? status == BUSY_UPDATING : status == CHECKING_FOR_WINNER) && 
      @               busy == notDone();
      @*/
    public void update() {
        //@ loop_invariant 0 <= x && x <= width;
        //@ loop_invariant board_has_valid_dimensions; 
        for(int x=0;x<width;x++){
            int bottom=height-1;
            //@ loop_invariant -1 <= bottom && bottom <= height - 1;
            //@ loop_invariant board_has_valid_dimensions;
            //@ loop_invariant (\forall int i; i > bottom && i <= height - 1; board[x][i] != Empty);
            while(bottom >= 0 && board[x][bottom] != Empty) bottom--;
            
            if (bottom > 0) {
                //@ loop_invariant 0 <= y && y <= bottom;
                //@ loop_invariant board_has_valid_dimensions;
                //@ loop_invariant board[x] == \old(board[x]);
                for(int y=bottom;y>0;y--) {
                  assignColumn(x, y, y - 1);
                }
                
                zero(x, 0);
            }
        }
        busy = notDone();
        //@ set status = busy ? BUSY_UPDATING : CHECKING_FOR_WINNER;
    }
    
    /**
     * assignColumn() requires the status to be BUSY_UPDATING, because this method can only be called when tokens fall down.
     * The requirements on i,j and k prevent ArrayIndexOutOfBoundsExceptions.
     * assignColumn() ensures GameBoard remains in the same status. 
     * Furthermore it ensures (using the last three forall's) that the board remains the same for every field that is not updated.
     */
    
    /*@ normal_behavior
      @   requires    status == BUSY_UPDATING &&
      @               j != k &&
      @               0 <= i && i < width &&
      @               0 <= j && j < height &&
      @               0 <= k && k < height;
      @   ensures     status == \old(status) &&
      @               board[i][j] == board[i][k] &&
      @               (\forall int x; 0 <= x && x < width && x != i; board[x][j] == \old(board[x][j])) &&
      @               (\forall int y; 0 <= y && y < height && y != j; board[i][y] == \old(board[i][y])) &&
      @               (\forall int x, y; 0 <= x && x < width && 0 <= y && y < height && (x != i && y != j); board[x][y] == \old(board[x][y]));
      @*/
    private void assignColumn(int i, int j, int k) {
      assign(board[i], j, k);
    }
    
    /**
     * assign() requires the status to be BUSY_UPDATING, because this method can only be called when tokens fall down.
     * The requirements on to and from prevent ArrayOutOfBoundsExceptions.
     * The non_null clause prevent NullPointerExceptions.
     * assign() ensures that GameBoard remains in the same status.
     * Furthermore it ensures that no field is changed except for the field with index to.
     */
    
    /*@ normal_behavior
      @   requires    status == BUSY_UPDATING &&
      @               to != from &&
      @               0 <= to && to < column.length &&
      @               0 <= from && from < column.length;
      @   ensures     status == \old(status) &&
      @               column[to] == column[from] &&
      @               (\forall int i; 0 <= i && i < column.length && i != to; column[i] == \old(column[i]));
      @*/
    private void assign(/*@ non_null @*/ byte[] column, int to, int from) {
      column[to] = column[from];
    }
    
    /**
     * zero() requires the status to be BUSY_UPDATING, because this can only be used when tokens need to fall down.
     * The requirements on x and y prevent ArrayIndexOutOfBoundsExceptions.
     * zero() ensures the status remains the same and board[x][y] == Empty.
     */
    
    /*@ normal_behavior
      @   requires    status == BUSY_UPDATING &&
      @               0 <= x && x < width &&
      @               0 <= y && y < height;
      @   ensures     status == \old(status) &&
      @               board[x][y] == Empty;
      @*/
    private void zero(int x, int y) {
      board[x][y] = Empty;
    }
    
    /**
     * status() requires the status not to be UNINITIALIZED and not BUSY_UPDATING.
     * If the status is UNINITIALIZED then status() would return "illegal state".
     * If the status is BUSY_UPDATING then there can not be a check for a winner, because a token is still falling down.
     * status ensures that GameBoard remains in the same status.
     * Furthermore it ensures that the result of this method is the correct string.
     */
    
    /*@ normal_behavior
      @   requires    status != UNINITIALIZED &&
      @               status != BUSY_UPDATING;
      @   ensures     (status == \old(status)) &&
      @               (\result == "busy" || \result == "tie" || \result == "won by X" || \result == "won by O" || \result == "next move for X" || \result == "next move for O") &&
      @               (busy ==> \result == "busy") &&
      @               ((!busy && gameOver()) ==> (\result == (winner == Empty ? "tie" : (winner == Cross ? "won by X" : "won by O")))) &&
      @               ((!busy && !gameOver()) ==> (\result == (turn == Cross ? "next move for X" : "next move for O"))); 
      @*/
    public String status(){
        if(busy) return "busy";
        if(gameOver()){
            switch(winner){
                case Empty: return "tie";
                case Cross: return "won by X";
                case Circle: return "won by O";
            }
        } else {
            switch(turn){
                case Cross: return "next move for X";
                case Circle: return "next move for O";
            }
        }
        //@ assert false;
        return "illegal state";
    }
}

